\section{Introduction}
\begin{frame}{Paper}
\begin{itemize}
\item \underline{Memoised} Garbage Collection for Software Model Checking \pause
\item \emph{To Memoise}: Storing an evaluated expression such there is no need to re-evaluate it again later. \pause
\item \emph{Software Model Checking} much like JPF (Java Path Finder); validating implemented systems.
\end{itemize}
\end{frame}

\begin{frame}{Paper}
\begin{itemize}
\item Need for a new algorithm for garbage collecting. \pause
\item Software model checkers spend up to half of their time garbage collecting (\emph{GC}).\pause
\item Introduced \emph{Memoised Garbage Collection} (\underline{MGC}) to replace \emph{Mark and Sweep} (\underline{M\&S}).
\end{itemize}
\end{frame}

\begin{frame}{GC for model checking}
\begin{itemize}
\item GC is normally used from freeing up memory in the heap. \pause
\item GC for model checking has an extra important purpose. \pause
\item Model checkers attempt to reduce the state space by using heap symmetry detection. \pause
\item Before we can check for symmetry all garbage needs to be collected.
\end{itemize}
\end{frame}

\begin{frame}{Moonwalker and MGC}
\begin{itemize}
\item MGC is implemented in a tool called \emph{Moonwalker}, by Theo Ruys, Niels Aan de Brugh (University of Twente) and Viet Yen Nguyen (Aachen University).\pause
\item \emph{Moon}: an anagram of Mono which is an open source implementation of Microsoft .NET framework.\pause
\item \emph{Walker}: nature of the tool; walking state space of Microsofts Common Intermediate Language (CIL) bytecode programs.\pause
\item Moonwalker was previously known as MMC (Mono Model Checker).\pause
\item So Moonwalker can validate programs written in C\# (checking for deadlocks, dataraces, etc...).
\end{itemize}
\end{frame}

\begin{frame}{Short example}
For those not all to familiar with JPF:
\begin{enumerate}
\item Install the Mono framework (version 1.2.6!) from \url{www.mono-project.com}, runs on Mac OS X, Linux and Windows.\pause
\item Write a Deadlock.cs (= a program which can deadlock on say monitors.)\pause
\item Compile it; \emph{\$ msc Deadlock.cs}\pause
\item Run moonwalker; \emph{\$ mono moonwalker.exe Deadlock.exe}\pause
\item Inspect the trace; \emph{\$ cat \tiny{(type)} \normalsize Deadlock.exe.trace}\pause
\end{enumerate}
\end{frame}

\begin{frame}[fragile]{Deadlock.cs (the locks)}
\begin{lstlisting}[language=java]
class PossibleDeadlock {
    object l1 = new object();
    object l2 = new object();
}
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Deadlock.cs (the get methods)}
\begin{lstlisting}[language=java]
public void Get12() {
    lock (l1) {
        lock (l2) {
            System.Console.WriteLine(
                "Got locks l1 and l2"
            );
        }
    }
}
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Deadlock.cs (the get methods)}
\begin{lstlisting}[language=java]
public void Get21() {
    lock (l2) {
        lock (l1) {
            System.Console.WriteLine(
                "Got locks l2 and l1"
            );
        }
    }
}
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Deadlock.cs (the main method)}
\begin{lstlisting}[language=java]
public static void Main(string[] args) {
    PossibleDeadlock dl = new PossibleDeadlock();
    Thread t1 = new Thread(
        new ThreadStart(dl.Get12)
    ); 
    t1.Start();
    Thread t2 = new Thread(
        new ThreadStart(dl.Get21)
    );
    t2.Start();
}
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Deadlock.exe.trace (the trace)}
\begin{lstlisting}[language=java]
- thread: 0 |_ 0000 newobj PossibleDeadlock::.ctor() on stack []
- thread: 0     |_ 0000 ldarg.0  on stack []
- thread: 0        0001 newobj Object::.ctor() on stack [Alloc(4)]
- thread: 0         |_ 0000 ret  on stack []
- thread: 0      ____________|
- thread: 0     |_ System.Void Deadlock/PossibleDeadlock::.ctor()
- thread: 0        0006 stfld PossibleDeadlock::l1 on stack [Alloc(4), Alloc(5)]
- thread: 0        0011 ldarg.0  on stack []
- thread: 0        0012 newobj Object::.ctor() on stack [Alloc(4)]
- thread: 0         |_ 0000 ret  on stack []
- thread: 0      ____________|
- thread: 0     |_ System.Void Deadlock/PossibleDeadlock::.ctor()
- thread: 0        0017 stfld PossibleDeadlock::l2 on stack [Alloc(4), Alloc(6)]
\end{lstlisting}
\end{frame}

\begin{frame}{Deadlock.exe.trace (what it tells us)}
It tells us that:
\begin{enumerate}
\item Thread 1 acquires lock1
\item Thread 2 acquires lock2
\item Thread 1 tries to acquire lock2
\item Thread 2 tries to acquire lock1
\item Thread 1 does not release lock1 before it has acquired lock2
\item Deadlock!
\end{enumerate}
A model checker tries to find one trace for this deadlock (a witness) in the model.
\end{frame}

\begin{frame}{A lot of GC}
\includegraphics[scale=.25]{img/time.png}
\begin{itemize}
\item \emph{GC}: Garbage collecting
\item \emph{State}: State storage
\item \emph{DFS}: State exploration
\end{itemize}
\end{frame}

\begin{frame}{Our focus}
\begin{itemize}
\item Introduced \emph{Memoised Garbage Collection} to replace \emph{Mark and Sweep}.\pause
\item Paper focuses on two aspects; the MGC algorithm and a benchmark of this algorithm.\pause
\item We focus mainly on the algorithm and a little on its benchmark.
\end{itemize}
\end{frame}
